COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%monadi[w85,jmc]		Decidability of monadic predicate calculus
C00010 ENDMK
C⊗;
%monadi[w85,jmc]		Decidability of monadic predicate calculus

\input jmcmac.tex[1,smc]
\title{A Normal Form for Monadic Formulas}

\vskip .5 in

Abstract: A normal form is given for formulas of the monadic first
order predicate calculus.  The form is closely related to some
proofs of the decidability of that calculus, but it seems to be
new and came up in extending decidability to circumscription for
monadic formulas.
\bigskip
\whentexed{monadi.tex[w85,jmc]}
\eject

	First consider closed monadic formulas involving the
predicate symbols $P↓1,\ldots,P↓n$.  Each such formula $E$ is equivalent
to a formula $normal(E)$ that is propositional in the $2↑n$ formulas
$L↓{\epsilon↓1\ldots \epsilon↓n}$
 defined by
$∃x.(¬)↑{\epsilon↓1}P↓1(x)∧\ldots∧(¬)↑{\epsilon↓n}P↓n(x)$.  Here the powers
of $¬$ mean that $¬$ is omitted if the power is $0$ and included
if the power is $1$.  That's our theorem.

	Intuitively, each $L↓{\epsilon↓1\ldots \epsilon↓n}$ says whether a
certain kind of element exists in an interpretation.  There are
$2↑n$ kinds of elements and an interpretation is characterized
by which kinds of elements exist.  The same is true for predicate
calculus in general, but then there are an infinite number of
kinds of elements.  Of course $normal(E)$ is often very much longer
than $E$.  If $E$ is a theorem, then $normal(E)$ will be a propositional
tautology in its constituents.

	In order to prove the theorem we must first generalize it
to include open formulas.  Suppose $w↓1,\ldots,w↓m$ are the free
variables of $E$.  There is still a propositional normal form, but in addition
to the
$L↓{\epsilon↓1\ldots \epsilon↓n}$,
$normal(E)$
may contain any of the $2↑nm$ formulas
$R↓{\epsilon↓1\ldots \epsilon↓n}(w↓k)$
defined by
$(¬)↑{\epsilon↓1}P↓1(w↓k)∧\ldots∧(¬)↑{\epsilon↓n}P↓n(w↓k)$
as propositional constituents.

	The proof is by induction on the structure of the formula,
so we must prove that the representation is possible for literals
and that property is preserved when formulas are combined by $∧$ and $∨$
and prefixed by $¬$ and existential quantifiers.
%  In order to avoid
%so many subscripts, we shall state and prove precise theorems for
%the case of two predicates, but the general case works exactly in
%the same way.  The greater concreteness of the two predicate case
%adds more understanding than is lost by the specialization.

\noindent{\bf Theorem 1:}
Every first order predicate calculus formula involving
predicate symbols $P↓1,\ldots,P↓n$ and individual variables $w↓1,\ldots,w↓m$
is representable as a disjunction of conjunctions.  Each conjunct
is either an
$L↓{\epsilon↓1\ldots \epsilon↓n}$,
of the form
$¬L↓{\epsilon↓1\ldots \epsilon↓n}$
or one of the
$R↓{\epsilon↓1\ldots \epsilon↓n}(w↓k)$.  Only one $R$ involving a particular
$w↓k$ can occur in a conjunction.  (Since the distinct $R$s are
contradictory, having two of them would make the conjunction always false
and therefore omittable).

1. Every elementary formula $P↓i(w↓k)$ is expressible in the stated
form.  For example, if $n=2$, we have
%
$$P↓1(w) ≡ (P↓1(w)∧P↓2(w)) ∨ (P↓1(w)∧¬P↓2(w)) ≡ R↓{00}(w)∨R↓{01}(w)$$.

2. If $E$ and $F$ are expressible then so is $E∨F$.  The disjunction
is merely longer.  Of course and duplicate conjuncts should be omitted.

3. If $E$ and $F$ are expressible then so is $E∧F$.  This requires
applying the distributive law of conjunction over disjunction and
may greatly lengthen the formula.  However, if any conjunct contains
different
$R↓{\epsilon↓1\ldots \epsilon↓n}(w↓k)$
with the same $w↓k$, it can be omitted since they are contradictory.

4. If $E$ is expressible then so is $¬E$.  This involves using
de Morgan's law and distributing.  Again it can get long and
again conjunctions with contradictory conjuncts must be omitted.

5. If $E$ is expressible then so is $∃w↓k.E$.  The quantifier
distributes over the terms of the disjunction and so is applied
to each conjunct separately.  Within a conjunct at most one
$R↓{\epsilon↓1\ldots \epsilon↓n}(w↓k)$
can occur, and the quantifier converts it into
$L↓{\epsilon↓1\ldots \epsilon↓n}$ leaving the other conjuncts untouched.

This concludes the proof.  Note that universal quantifiers had
to be converted to existentials according to $∀x → ¬∃x¬$ which
will lengthen the formulas when the $¬$s are distributed.
\vfil\end